theory SynLang imports Main "thirdparty/Transitive-Closure/Transitive_Closure_List_Impl"

(* Authors: E. Ivanov, M. Strecker *)
(* A part of Isabelle formalization of a synchronous language *)
(* See http://www.irit.fr/~Martin.Strecker/Publications/clock_type_soundness.pdf *)

(* This file contains an implementation of a cyclic variable dependency checker *)
(* If {xi>xj | i,j} is a set of variable dependencies (xj depends on xi), we check if this set has no cycles *)
(* We implement a function (check_program), which checks if a program has no variable dependency cycles *)
(* We prove that this implementation is correct (see the last theorem) *)
(* The function check_program is used to generate a stand-alone dependency verifier in ML (Gencode.thy) *)

begin

datatype val_tp   = UnitT  | BoolT      | NatT      | PairT val_tp val_tp  -- "data type name: binary tree of basic type names"

datatype cst      = UnitC  | BoolC bool | NatC nat                         -- "literal"
datatype calcf    = PlusF                                                  -- "arithmetic operation name"
datatype specialf = AffsetF nat nat                                        -- "affine set"

datatype funid    = ConstF cst | SpecialF specialf  | CalcF calcf          -- "function name (constant, clock, arithmetic operation)"

datatype vals     = UnitV | BoolV bool | NatV nat | PairV vals vals

primrec vals_tp :: "vals \<Rightarrow> val_tp"
where
  "vals_tp UnitV = UnitT"
 |"vals_tp (BoolV b) = BoolT"
 |"vals_tp (NatV n) = NatT"
 |"vals_tp (PairV v v') = PairT (vals_tp v) (vals_tp v')"

datatype ('n,'v) canon_expr                                                -- "expression: binary tree of var names, fun applications; 'n - var names"
  = CanVar 'n
  | CanPairE "(('n,'v) canon_expr)" "(('n,'v) canon_expr)"
  | CanFun funid "(('n,'v) canon_expr)"

datatype 'n proc_header = ProcHeader 'n 'n                                 -- "proc header: interface name(?), implementation(?) name; 'n - proc names"
datatype 'n cname = Cname "('n proc_header)" 'n                            -- "tagged proc name for use in calls; 'n - tags/proc names"

datatype ('n,'v,'tp) canon_stmt                                            -- "statement; 'n - var names, 'v - values, 'tp - types"
  = CanEmptyStmt
  | CanCombin 'n "(('n,'v) canon_expr)"                                    -- "n = e"
  | CanPre 'n 'v 'n                                                        -- "n1 = v fby n2"
  | CanWhen 'n 'n 'n                                                       -- "n1 = n2 when n3"
  | CanDefault 'n 'n 'n                                                    -- "n1 = n2 default n3"
  | CanPar "(('n,'v,'tp) canon_stmt)" "(('n,'v,'tp) canon_stmt)"           -- "c1 \<parallel> c2"
  | CanPCall "('n cname)" "('n list)"                                      -- "<tagged fun name> ( n1, n2, ... )"
  | CanLetv 'n 'tp "(('n,'v,'tp) canon_stmt)"                              -- "local var declaration; let n:tp in c"

datatype 'n inter_typ = InterTyp "(val_tp)" (*"(('n,affset_tp) clexpr)"*)  -- "data type + clock type (for interface arguments ?)"
datatype ('n,'tp) var_types = VarTypes 'n 'tp                              -- "variable declaration; 'n - names, 'tp - types"
datatype ('n,'tp) interf                                                   -- "interface; 'n - var names, 'tp - types (i.e. inter_typ)"
  = Interf "'n" "(('n,'tp) var_types list)" "('n*'n) list"

fun get_var_types_name :: "('n,'tp) var_types \<Rightarrow> 'n"
where "get_var_types_name (VarTypes a b) = a"

fun get_var_types_type :: "('n,'tp) var_types \<Rightarrow> 'tp"
where "get_var_types_type (VarTypes a b) = b"

datatype ('n,'v,'tp) canon_proc                                            -- "procedure; 'n - var names, 'v - values, 'tp - types"
  = CanProc  "('n proc_header)" "('n,'tp) var_types list" "(('n,'v,'tp) canon_stmt)"   -- "(interf name, impl name), var decl list, body"

datatype ('n,'v,'tp) canon_program                                         -- "program - list of interfaces and list of procedures"
  = CanProgram "(('n,'tp) interf list)" "(('n,'v,'tp) canon_proc list)"

(*----------------------------------------------------------------------------------------------------------*)

fun is_noncyclic :: "('n \<times> 'n) list \<Rightarrow> bool"
where
  "is_noncyclic rel = (\<forall> a \<in> set (map fst rel). a \<notin> set ((memo_list_trancl rel) a))"

lemma is_noncyclic: "is_noncyclic rel = (\<forall> (a,b) \<in> (set rel)^+ . a \<noteq> b)"
apply(simp add:memo_list_trancl)
apply(auto)
by (metis Domain_iff fst_conv trancl_domain)

lemma noncycrefl: "is_noncyclic r = (irrefl ((set r)^+))"
by (subst is_noncyclic, auto simp add: irrefl_def)

(*----------------------------Data access functions---------------------------------------------------------------------*)


fun get_interf_name :: "('n,'n inter_typ) interf \<Rightarrow> 'n"
where
  "get_interf_name (Interf inm vtps deps) = inm"

fun get_interf_args :: "('n,'n inter_typ) interf \<Rightarrow> 'n list"
where
  "get_interf_args (Interf inm vtps deps) = (map get_var_types_name vtps)"

fun get_interf_deps :: "('n,'n inter_typ) interf \<Rightarrow> ('n \<times> 'n) list"
where
  "get_interf_deps (Interf inm vtps deps) = deps"

fun get_interf :: "('n,'n inter_typ) interf list \<Rightarrow> 'n \<Rightarrow> ('n,'n inter_typ) interf"
where
  "get_interf [] iname = (Interf iname [] [])"
 |"get_interf (interf # other) iname = (if ((get_interf_name interf)=iname) then interf else (get_interf other iname))"

fun get_proc_iname :: "('n,vals,'n inter_typ) canon_proc \<Rightarrow> 'n"    --"interface name"
where 
  "get_proc_iname (CanProc (ProcHeader iname _) _ body) = iname"

fun get_proc_body :: "('n,vals,'n inter_typ) canon_proc \<Rightarrow> ('n,vals,'n inter_typ) canon_stmt"
where
  "get_proc_body (CanProc (ProcHeader iname _) _ body) = body"

(*----------------------------------------------------------------------------------------------------------*)

fun var_renm :: "'n list \<Rightarrow> 'n list \<Rightarrow> 'n \<Rightarrow> 'n"
where
  "var_renm [] _ z = z"
 |"var_renm _ [] z = z"
 |"var_renm (x#xs) (y#ys) z = (if x=z then y else (var_renm xs ys z))"

fun interf_var_renm :: "('n,'n inter_typ) interf \<Rightarrow> 'n list \<Rightarrow> 'n \<Rightarrow> 'n"
where
  "interf_var_renm interf vfact x = var_renm (get_interf_args interf) vfact x"

(*--------------------------Dependency semantics--------------------------------------------------------------------------------*)

primrec sem_expr_deps :: "('n,'v) canon_expr \<Rightarrow> 'n set"
where
  "sem_expr_deps (CanVar v)       = {v}"
 |"sem_expr_deps (CanPairE e1 e2) = (sem_expr_deps e1) \<union> (sem_expr_deps e2)"
 |"sem_expr_deps (CanFun fid e)   = sem_expr_deps e"

fun sem_interf_deps_renm :: "('n,'n inter_typ) interf \<Rightarrow> 'n list \<Rightarrow> ('n \<times> 'n) set"
where
  "sem_interf_deps_renm interf vlist = { p . \<exists> (u,v) \<in> set (get_interf_deps interf) . p = ((interf_var_renm interf vlist u), (interf_var_renm interf vlist v))  }"

fun pass_closure :: "('n \<times> 'n) set \<Rightarrow> 'n \<Rightarrow> ('n \<times> 'n) set"
where
  "pass_closure r w = {(u,v) . (u,v) \<in> (r \<union> r O r) \<and> (u \<noteq> w) \<and> (v \<noteq> w)}"

(* sem_body_deps returns a set of pairs (u,v) "u depends on v" for a given statement *)
fun sem_body_deps :: "('n,'n inter_typ) interf list \<Rightarrow> ('n,'v,'tp) canon_stmt \<Rightarrow> ('n \<times> 'n) set"
where
  "sem_body_deps interfs CanEmptyStmt        = {}"
 |"sem_body_deps interfs (CanCombin v e)     = {p . \<exists> u . p = (v,u) \<and> u \<in> (sem_expr_deps e)}"
 |"sem_body_deps interfs (CanPre u val v)    = {(u,v)}"
 |"sem_body_deps interfs (CanWhen u v w)     = {(u,v),(u,w)}"
 |"sem_body_deps interfs (CanDefault u v w)  = {(u,v),(u,w)}"
 |"sem_body_deps interfs (CanPar stm1 stm2)  = ((sem_body_deps interfs stm1) \<union> (sem_body_deps interfs stm2))"
 |"sem_body_deps interfs (CanPCall (Cname (ProcHeader iname _) _) args) = sem_interf_deps_renm (get_interf interfs iname) args" --"deps from interface"
 |"sem_body_deps interfs (CanLetv w typ stm) = (pass_closure (sem_body_deps interfs stm) w)" --"u depends on v or u depends on w and w depends on v"

(* sem_body_tdeps defines semantics of the notion "x (transitively) depends y" *)
fun sem_body_tdeps :: "('n,'n inter_typ) interf list \<Rightarrow> ('n,'v,'tp) canon_stmt \<Rightarrow> ('n \<times> 'n) set"
where
  "sem_body_tdeps interfs stm = (sem_body_deps interfs stm)^+"

(*------------------------Dependency check implementation----------------------------------------------------------------------------------*)

primrec expr_deps :: "('n,'v) canon_expr \<Rightarrow> 'n list"
where
  "expr_deps (CanVar v)       = [v]"
 |"expr_deps (CanPairE e1 e2) = (expr_deps e1) @ (expr_deps e2)"
 |"expr_deps (CanFun fid e)   = expr_deps e"

fun interf_deps_renm :: "('n,'n inter_typ) interf \<Rightarrow> 'n list \<Rightarrow> ('n \<times> 'n) list"
where
  "interf_deps_renm interf vlist = (map (\<lambda> (u,v). ((interf_var_renm interf vlist u), (interf_var_renm interf vlist v))) (get_interf_deps interf))"

fun list_mul :: "('n \<times> 'n) list \<Rightarrow> ('n \<times> 'n) list \<Rightarrow> ('n \<times> 'n) list"
where
  "list_mul [] r = []"
 |"list_mul ((u,v) # other) r = (map (\<lambda> (x,y). (u,y)) (filter (\<lambda> (x,y). x = v) r)) @ (list_mul other r)"

lemma [simp]: "set (list_mul a b) = (set a) O (set b)"
apply(auto simp add: rel_comp_def)
apply(induct a)
apply(auto)
apply(auto)
apply(induct a)
apply(auto)
done

fun list_pass_closure :: "('n \<times> 'n) list \<Rightarrow> 'n \<Rightarrow> ('n \<times> 'n) list"
where
  "list_pass_closure r w = (filter (\<lambda> (u,v). u\<noteq>w \<and> v\<noteq>w) (r @ (list_mul r r)))"

lemma [simp]: "set (list_pass_closure r w) = pass_closure (set r) w" by (auto)

fun body_deps :: "('n,'n inter_typ) interf list \<Rightarrow> ('n,'v,'tp) canon_stmt \<Rightarrow> ('n \<times> 'n) list"
where
  "body_deps interfs CanEmptyStmt        = []"
 |"body_deps interfs (CanCombin v e)     = map (\<lambda> x. (v,x)) (expr_deps e)"
 |"body_deps interfs (CanPre u val v)    = [(u,v)]"
 |"body_deps interfs (CanWhen u v w)     = [(u,v),(u,w)]"
 |"body_deps interfs (CanDefault u v w)  = [(u,v),(u,w)]"
 |"body_deps interfs (CanPar stm1 stm2)  = (body_deps interfs stm1) @ (body_deps interfs stm2)"
 |"body_deps interfs (CanPCall (Cname (ProcHeader iname _) _) args) = interf_deps_renm (get_interf interfs iname) args"
 |"body_deps interfs (CanLetv w typ stm) = (list_pass_closure (body_deps interfs stm) w)"

(*----------------------------------------------------------------------------------------------------------*)

fun is_tcbase :: "('n \<times> 'n) list \<Rightarrow> ('n \<times> 'n) list \<Rightarrow> bool"
where
  "is_tcbase r1 r2 = (\<forall> (u,v) \<in> (set r1) . v \<in> set ((memo_list_trancl r2) u) )"

fun check_deps :: "'n list \<Rightarrow> ('n \<times> 'n) list \<Rightarrow> ('n \<times> 'n) list \<Rightarrow> bool"
where
  "check_deps args bdeps ideps = ((set (map fst ideps)) \<subseteq> (set args) \<and> (set (map snd ideps)) \<subseteq> (set args) \<and> (is_noncyclic ideps) \<and> (is_tcbase bdeps ideps))"

fun check_proc :: "[('n,'n inter_typ) interf list, ('n,vals,'n inter_typ) canon_proc] \<Rightarrow> bool"
where
  "check_proc interfs p = (check_deps (get_interf_args (get_interf interfs (get_proc_iname p))) (body_deps interfs (get_proc_body p)) (get_interf_deps (get_interf interfs (get_proc_iname p))))"

fun check_program :: "('n,vals,'n inter_typ) canon_program \<Rightarrow> bool"
where
  "check_program (CanProgram interfs procs) = (\<forall> p \<in> set procs. check_proc interfs p)"

(*------------------------Correctness of dependency check implementation------------------------------------------------------------*)

lemma [simp]: "(sem_expr_deps e) = set (expr_deps e)"
apply(induct e)
apply(auto)
done

lemma [simp]: "set (body_deps interfs stm) = (sem_body_deps interfs stm)"
apply(induct stm)
apply(auto simp add: image_def)
apply(case_tac cname)
apply(auto)
apply(case_tac proc_header)
apply(auto)
apply(case_tac cname)
apply(auto)
apply(case_tac proc_header)
apply(simp)
apply(auto)
done

fun sem_check_deps :: "'n list \<Rightarrow> ('n \<times> 'n) set \<Rightarrow> ('n \<times> 'n) list \<Rightarrow> bool"   
where
  "sem_check_deps args tbdeps ideps = ( ((set ideps)^+) \<subseteq> (set args) \<times> (set args) \<and> (irrefl ((set ideps)^+)) \<and> tbdeps \<subseteq> ((set ideps)^+) )"

fun sem_check_proc :: "[('n,'n inter_typ) interf list, ('n,vals,'n inter_typ) canon_proc] \<Rightarrow> bool"
where
  "sem_check_proc interfs p = (sem_check_deps (get_interf_args (get_interf interfs (get_proc_iname p))) (sem_body_tdeps interfs (get_proc_body p)) (get_interf_deps (get_interf interfs (get_proc_iname p))))"

fun sem_check_program :: "('n,vals,'n inter_typ) canon_program \<Rightarrow> bool"
where
  "sem_check_program (CanProgram interfs procs) = (\<forall> p \<in> set procs. sem_check_proc interfs p)"

lemma trsqr: "((r^+) \<subseteq> a \<times> a) = (r \<subseteq> a \<times> a)"
proof (auto, metis SigmaE2 in_mono trancl_subset_Sigma)
fix aa
fix b
assume a1:"r \<subseteq> a \<times> a"
assume a2:" (aa,b) \<in> (r^+)"
from a1 have "(r^+) \<subseteq> a \<times> a"
by (metis trancl_subset_Sigma)
from a2 and this show "b \<in> a" by auto
qed

lemma  mytrcompl: " ((a^+) \<subseteq> (b^+)) = (a \<subseteq> (b^+))"
proof (rule iffI, force)
assume a1:"a \<subseteq> (b^+)"
show "(a^+) \<subseteq> (b^+)" 
  proof -
    obtain c where a2:"c = (b^+)" by auto
    then have a3:"trans (c)" by auto
    from a1 and a2 have "a \<subseteq> c" by auto
    from this and a3 have "(a^+) \<subseteq> c" by (auto, metis trancl_id trancl_mono)
    from this and a2 have " (a^+) \<subseteq> (b^+)" by auto
    then show ?thesis by auto
  qed
qed

lemma is_tcbase: "is_tcbase r1 r2 = ((set r1)^+ \<subseteq> (set r2)^+)"
apply(simp add:memo_list_trancl)
apply(subst mytrcompl)
apply(auto)
done

lemma check_deps: "check_deps args bdeps ideps = sem_check_deps args ((set bdeps)^+) ideps"
apply(auto simp add: trsqr noncycrefl is_tcbase memo_list_trancl irrefl_def)
apply(thin_tac "fst ` set ideps \<subseteq> set args")
apply(thin_tac "snd ` set ideps \<subseteq> set args")
apply (metis Domain_iff fst_conv trancl_domain)
apply(subgoal_tac "((set bdeps)^+) \<subseteq> (set ideps)^+")
apply(force)
apply(subst mytrcompl)
apply(auto)
done

lemma check_proc: "check_proc interfs p = sem_check_proc interfs p"
apply(subst check_proc.simps)
apply(subst sem_check_proc.simps)
apply(subst check_deps)
apply(auto)
done

theorem "check_program p = sem_check_program p"
apply(case_tac p)
apply(clarify)
apply(subst check_program.simps)
apply(subst sem_check_program.simps)
apply(subst Ball_def)
apply(subst check_proc)
apply(auto)
done

end
